Nuprl Lemma : es-LnkTag-deq_wf 0,22
es-LnkTag-deq  EqDecider(IdLnkId) 
latex

Definitionses-LnkTag-deq, product-deq(A;B;a;b), x:A. B(x), IdLnk, Id, IdLnkDeq, t  T, IdDeq
Lemmasid-deq wf, idlnk-deq wf, Id wf, IdLnk wf, product-deq wf

origin